Inference at * 1 
Iof proof for Lemma spread to pi12:



1. A : Type
2. B : AType
3. p : x:A  B(x)
4. C : Type
5. b : x:AB(x)C
  let x,y = p in b(x,y) = b(p.1,p.2) 

latex

 by ((D 3) 
CollapseTHEN (AbReduce 0)) 

latex

C1: 

C1: 3. x : A
C1: 4. p1 : B(x)
C1: 5. C : Type
C1: 6. b : x:AB(x)C
C1:   b(x,p1) = b(x,p1)
C.

Definitions

t.2, t.1